(assert (forall ((q0 (_ BitVec 9)) (q1 (_ BitVec 9)) (q2 (_ BitVec 9)) (q3 (_ BitVec 9)) (q4 (_ BitVec 8))) (=> (bvuge q1 q1) (distinct (bvashr q4 q4) q4))))
(assert (forall ((q5 (_ BitVec 9)) (q6 (_ BitVec 9)) (q7 Bool)) (=> (= q5 (bvsdiv q6 q5)) (or q7 q7 q7 q7 q7 q7 q7 q7))))
(assert (forall ((q8 (_ BitVec 9)) (q9 (_ BitVec 9)) (q10 (_ BitVec 8))) (=> (= q10 q10) (= q9 (bvashr q8 (bvxor q9 q9 q9 q9))))))
(assert (forall ((q11 (_ BitVec 9)) (q12 (_ BitVec 9)) (q13 (_ BitVec 8))) (=> (= q13 q13) (bvsle (bvor q12 q11) (bvsdiv q12 q12)))))
(assert (forall ((q14 (_ BitVec 9)) (q15 (_ BitVec 9)) (q16 (_ BitVec 12))) (=> (bvuge (bvor q16 q16) (bvand (bvnot q16) (bvnot q16))) (bvsgt q15 q14))))
(assert (forall ((q17 (_ BitVec 9)) (q18 (_ BitVec 9)) (q19 (_ BitVec 9)) (q20 (_ BitVec 9)) (q21 Bool)) (=> (xor q21 q21 q21 q21 q21 q21 q21 q21) (distinct (bvnand q17 q18) (bvnand q17 q18)))))
(assert (forall ((q22 (_ BitVec 9)) (q23 (_ BitVec 9)) (q24 (_ BitVec 9)) (q25 (_ BitVec 12))) (=> (distinct (bvudiv q25 q25) (bvudiv q25 q25)) (bvslt q22 q22))))
(assert (forall ((q26 (_ BitVec 9)) (q27 Bool)) (=> (= q26 q26) (xor q27 q27 q27 q27 q27))))
(assert (forall ((q28 (_ BitVec 9)) (q29 (_ BitVec 9)) (q30 (_ BitVec 9)) (q31 (_ BitVec 10))) (=> (= q30 q30) (bvsgt q31 (bvsmod q31 q31)))))
(assert (forall ((q39 (_ BitVec 9)) (q40 (_ BitVec 9)) (q41 (_ BitVec 9)) (q42 (_ BitVec 9)) (q43 (_ BitVec 8))) (=> (distinct q39 (bvadd q39 q42)) (= (bvnot (bvurem ((_ extract 7 0) q43) q43)) q43))))
(check-sat)
